$\forall$$T$:Type, $Q$:(($T$ List)$\rightarrow$prop\{i:l\}).
\\[0ex]$Q$([])
\\[0ex]$\Rightarrow$ ($\forall$${\it ys}$:($T$ List), $y$:$T$. $Q$(${\it ys}$) $\Rightarrow$ $Q$(append(${\it ys}$; cons($y$; []))))
\\[0ex]$\Rightarrow$ guard(($\forall$${\it zs}$:($T$ List). $Q$(${\it zs}$)))